0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 554 ms)
↳12 BOUNDS(1, n^2)
isort(Cons(x, xs), r) → isort(xs, insert(x, r))
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
isort(Nil, r) → r
insert(x, Nil) → Cons(x, Nil)
inssort(xs) → isort(xs, Nil)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs))
insert[Ite][False][Ite](True, x, r) → Cons(x, r)
isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](<(x', x), x', Cons(x, xs)) [1]
isort(Nil, r) → r [1]
insert(x, Nil) → Cons(x, Nil) [1]
inssort(xs) → isort(xs, Nil) [1]
<(S(x), S(y)) → <(x, y) [0]
<(0, S(y)) → True [0]
<(x, 0) → False [0]
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite][False][Ite](True, x, r) → Cons(x, r) [0]
| < => lt |
isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](lt(x', x), x', Cons(x, xs)) [1]
isort(Nil, r) → r [1]
insert(x, Nil) → Cons(x, Nil) [1]
inssort(xs) → isort(xs, Nil) [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite][False][Ite](True, x, r) → Cons(x, r) [0]
isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](lt(x', x), x', Cons(x, xs)) [1]
isort(Nil, r) → r [1]
insert(x, Nil) → Cons(x, Nil) [1]
inssort(xs) → isort(xs, Nil) [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite][False][Ite](True, x, r) → Cons(x, r) [0]
| isort :: Cons:Nil → Cons:Nil → Cons:Nil Cons :: S:0 → Cons:Nil → Cons:Nil insert :: S:0 → Cons:Nil → Cons:Nil insert[Ite][False][Ite] :: True:False → S:0 → Cons:Nil → Cons:Nil lt :: S:0 → S:0 → True:False Nil :: Cons:Nil inssort :: Cons:Nil → Cons:Nil S :: S:0 → S:0 0 :: S:0 True :: True:False False :: True:False |
lt(v0, v1) → null_lt [0]
insert[Ite][False][Ite](v0, v1, v2) → null_insert[Ite][False][Ite] [0]
isort(v0, v1) → null_isort [0]
insert(v0, v1) → null_insert [0]
null_lt, null_insert[Ite][False][Ite], null_isort, null_insert
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Nil => 0
0 => 0
True => 2
False => 1
null_lt => 0
null_insert[Ite][False][Ite] => 0
null_isort => 0
null_insert => 0
insert(z, z') -{ 1 }→ insert[Ite][False][Ite](lt(x', x), x', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, x >= 0, z = x'
insert(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
insert(z, z') -{ 1 }→ 1 + x + 0 :|: x >= 0, z = x, z' = 0
insert[Ite][False][Ite](z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
insert[Ite][False][Ite](z, z', z'') -{ 0 }→ 1 + x + r :|: z = 2, z'' = r, r >= 0, z' = x, x >= 0
insert[Ite][False][Ite](z, z', z'') -{ 0 }→ 1 + x + insert(x', xs) :|: z' = x', xs >= 0, z = 1, x' >= 0, x >= 0, z'' = 1 + x + xs
inssort(z) -{ 1 }→ isort(xs, 0) :|: xs >= 0, z = xs
isort(z, z') -{ 1 }→ r :|: r >= 0, z = 0, z' = r
isort(z, z') -{ 1 }→ isort(xs, insert(x, r)) :|: z = 1 + x + xs, xs >= 0, r >= 0, x >= 0, z' = r
isort(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
lt(z, z') -{ 0 }→ lt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
lt(z, z') -{ 0 }→ 2 :|: z' = 1 + y, y >= 0, z = 0
lt(z, z') -{ 0 }→ 1 :|: x >= 0, z = x, z' = 0
lt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V15),0,[isort(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[insert(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[inssort(V, Out)],[V >= 0]). eq(start(V, V1, V15),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[fun(V, V1, V15, Out)],[V >= 0,V1 >= 0,V15 >= 0]). eq(isort(V, V1, Out),1,[insert(V3, V4, Ret1),isort(V2, Ret1, Ret)],[Out = Ret,V = 1 + V2 + V3,V2 >= 0,V4 >= 0,V3 >= 0,V1 = V4]). eq(insert(V, V1, Out),1,[lt(V5, V6, Ret0),fun(Ret0, V5, 1 + V6 + V7, Ret2)],[Out = Ret2,V7 >= 0,V1 = 1 + V6 + V7,V5 >= 0,V6 >= 0,V = V5]). eq(isort(V, V1, Out),1,[],[Out = V8,V8 >= 0,V = 0,V1 = V8]). eq(insert(V, V1, Out),1,[],[Out = 1 + V9,V9 >= 0,V = V9,V1 = 0]). eq(inssort(V, Out),1,[isort(V10, 0, Ret3)],[Out = Ret3,V10 >= 0,V = V10]). eq(lt(V, V1, Out),0,[lt(V11, V12, Ret4)],[Out = Ret4,V1 = 1 + V12,V11 >= 0,V12 >= 0,V = 1 + V11]). eq(lt(V, V1, Out),0,[],[Out = 2,V1 = 1 + V13,V13 >= 0,V = 0]). eq(lt(V, V1, Out),0,[],[Out = 1,V14 >= 0,V = V14,V1 = 0]). eq(fun(V, V1, V15, Out),0,[insert(V17, V18, Ret11)],[Out = 1 + Ret11 + V16,V1 = V17,V18 >= 0,V = 1,V17 >= 0,V16 >= 0,V15 = 1 + V16 + V18]). eq(fun(V, V1, V15, Out),0,[],[Out = 1 + V19 + V20,V = 2,V15 = V20,V20 >= 0,V1 = V19,V19 >= 0]). eq(lt(V, V1, Out),0,[],[Out = 0,V21 >= 0,V22 >= 0,V = V21,V1 = V22]). eq(fun(V, V1, V15, Out),0,[],[Out = 0,V23 >= 0,V15 = V24,V25 >= 0,V = V23,V1 = V25,V24 >= 0]). eq(isort(V, V1, Out),0,[],[Out = 0,V26 >= 0,V27 >= 0,V = V26,V1 = V27]). eq(insert(V, V1, Out),0,[],[Out = 0,V28 >= 0,V29 >= 0,V = V28,V1 = V29]). input_output_vars(isort(V,V1,Out),[V,V1],[Out]). input_output_vars(insert(V,V1,Out),[V,V1],[Out]). input_output_vars(inssort(V,Out),[V],[Out]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,V15,Out),[V,V1,V15],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [lt/3]
1. recursive : [fun/4,insert/3]
2. recursive : [isort/3]
3. non_recursive : [inssort/2]
4. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into lt/3
1. SCC is partially evaluated into insert/3
2. SCC is partially evaluated into isort/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations lt/3
* CE 19 is refined into CE [20]
* CE 18 is refined into CE [21]
* CE 17 is refined into CE [22]
* CE 16 is refined into CE [23]
### Cost equations --> "Loop" of lt/3
* CEs [23] --> Loop 13
* CEs [20] --> Loop 14
* CEs [21] --> Loop 15
* CEs [22] --> Loop 16
### Ranking functions of CR lt(V,V1,Out)
* RF of phase [13]: [V,V1]
#### Partial ranking functions of CR lt(V,V1,Out)
* Partial RF of phase [13]:
- RF of loop [13:1]:
V
V1
### Specialization of cost equations insert/3
* CE 9 is refined into CE [24,25]
* CE 8 is refined into CE [26,27,28,29,30]
* CE 12 is refined into CE [31]
* CE 11 is refined into CE [32]
* CE 10 is refined into CE [33,34]
### Cost equations --> "Loop" of insert/3
* CEs [33,34] --> Loop 17
* CEs [25] --> Loop 18
* CEs [32] --> Loop 19
* CEs [24] --> Loop 20
* CEs [26,27,28,29,30,31] --> Loop 21
### Ranking functions of CR insert(V,V1,Out)
* RF of phase [17]: [V1]
#### Partial ranking functions of CR insert(V,V1,Out)
* Partial RF of phase [17]:
- RF of loop [17:1]:
V1
### Specialization of cost equations isort/3
* CE 15 is refined into CE [35]
* CE 14 is refined into CE [36]
* CE 13 is refined into CE [37,38,39,40]
### Cost equations --> "Loop" of isort/3
* CEs [40] --> Loop 22
* CEs [37] --> Loop 23
* CEs [39] --> Loop 24
* CEs [38] --> Loop 25
* CEs [35] --> Loop 26
* CEs [36] --> Loop 27
### Ranking functions of CR isort(V,V1,Out)
* RF of phase [22,23,24,25]: [V]
#### Partial ranking functions of CR isort(V,V1,Out)
* Partial RF of phase [22,23,24,25]:
- RF of loop [22:1,23:1,24:1,25:1]:
V
- RF of loop [25:1]:
-V1+1 depends on loops [22:1,24:1]
### Specialization of cost equations start/3
* CE 2 is refined into CE [41]
* CE 3 is refined into CE [42,43,44,45]
* CE 4 is refined into CE [46,47,48]
* CE 5 is refined into CE [49,50,51,52]
* CE 6 is refined into CE [53,54,55]
* CE 7 is refined into CE [56,57,58,59,60]
### Cost equations --> "Loop" of start/3
* CEs [50,57] --> Loop 28
* CEs [42,43,44,45] --> Loop 29
* CEs [41,46,47,48,49,51,52,53,54,55,56,58,59,60] --> Loop 30
### Ranking functions of CR start(V,V1,V15)
#### Partial ranking functions of CR start(V,V1,V15)
Computing Bounds
=====================================
#### Cost of chains of lt(V,V1,Out):
* Chain [[13],16]: 0
with precondition: [Out=2,V>=1,V1>=V+1]
* Chain [[13],15]: 0
with precondition: [Out=1,V1>=1,V>=V1]
* Chain [[13],14]: 0
with precondition: [Out=0,V>=1,V1>=1]
* Chain [16]: 0
with precondition: [V=0,Out=2,V1>=1]
* Chain [15]: 0
with precondition: [V1=0,Out=1,V>=0]
* Chain [14]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of insert(V,V1,Out):
* Chain [[17],21]: 1*it(17)+1
Such that:it(17) =< Out
with precondition: [V>=0,Out>=1,V1>=Out]
* Chain [[17],20]: 1*it(17)+1
Such that:it(17) =< Out
with precondition: [V=0,V1+1=Out,V1>=3]
* Chain [[17],19]: 1*it(17)+1
Such that:it(17) =< V1
with precondition: [V+V1+1=Out,V>=0,V1>=1]
* Chain [[17],18]: 1*it(17)+1
Such that:it(17) =< 2*V1-Out
with precondition: [V+V1+1=Out,V>=1,V1>=V+3]
* Chain [21]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [20]: 1
with precondition: [V=0,V1+1=Out,V1>=2]
* Chain [19]: 1
with precondition: [V1=0,V+1=Out,V>=0]
* Chain [18]: 1
with precondition: [V+V1+1=Out,V>=1,V1>=V+2]
#### Cost of chains of isort(V,V1,Out):
* Chain [[22,23,24,25],27]: 6*it(22)+2*it(25)+2*s(12)+1*s(13)+1*s(14)+1
Such that:aux(10) =< V+V1
aux(7) =< -V1+1
aux(12) =< V
it(22) =< aux(12)
it(25) =< aux(12)
aux(4) =< aux(10)
aux(2) =< aux(10)-1
s(12) =< it(22)*aux(10)
it(25) =< aux(12)+aux(7)
s(13) =< it(22)*aux(4)
s(14) =< it(22)*aux(2)
with precondition: [V>=1,V1>=0,Out>=0,V+V1>=Out]
* Chain [[22,23,24,25],26]: 6*it(22)+2*it(25)+2*s(12)+1*s(13)+1*s(14)+0
Such that:aux(10) =< V+V1
aux(7) =< -V1+1
aux(13) =< V
it(22) =< aux(13)
it(25) =< aux(13)
aux(4) =< aux(10)
aux(2) =< aux(10)-1
s(12) =< it(22)*aux(10)
it(25) =< aux(13)+aux(7)
s(13) =< it(22)*aux(4)
s(14) =< it(22)*aux(2)
with precondition: [Out=0,V>=1,V1>=0]
* Chain [27]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of start(V,V1,V15):
* Chain [30]: 24*s(29)+4*s(30)+4*s(33)+2*s(34)+2*s(35)+2*s(46)+1*s(47)+1*s(48)+4*s(54)+4*s(57)+2*s(58)+2*s(59)+2
Such that:s(47) =< -V+V1
s(48) =< V+V1+1
aux(16) =< 1
aux(17) =< V
aux(18) =< V+V1
aux(19) =< -V1+1
aux(20) =< V1
s(46) =< aux(20)
s(29) =< aux(17)
s(54) =< aux(17)
s(55) =< aux(17)
s(56) =< aux(17)-1
s(57) =< s(29)*aux(17)
s(54) =< aux(17)+aux(16)
s(58) =< s(29)*s(55)
s(59) =< s(29)*s(56)
s(30) =< aux(17)
s(31) =< aux(18)
s(32) =< aux(18)-1
s(33) =< s(29)*aux(18)
s(30) =< aux(17)+aux(19)
s(34) =< s(29)*s(31)
s(35) =< s(29)*s(32)
with precondition: [V>=0]
* Chain [29]: 2*s(70)+1*s(71)+1*s(72)+1
Such that:s(71) =< -V1+V15
s(72) =< V1+V15
aux(21) =< V15
s(70) =< aux(21)
with precondition: [V=1,V1>=0,V15>=1]
* Chain [28]: 1
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V15):
-------------------------------------
* Chain [30] with precondition: [V>=0]
- Upper bound: 32*V+2+6*V*V+nat(V1)*2+nat(V-1)*2*V+nat(nat(V+V1)+ -1)*2*V+nat(V+V1)*6*V+nat(-V+V1)+nat(V+V1+1)
- Complexity: n^2
* Chain [29] with precondition: [V=1,V1>=0,V15>=1]
- Upper bound: V1+3*V15+1+nat(-V1+V15)
- Complexity: n
* Chain [28] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
### Maximum cost of start(V,V1,V15): max([nat(V15)*2+nat(V1+V15)+nat(-V1+V15),32*V+1+6*V*V+nat(V1)*2+nat(V-1)*2*V+nat(nat(V+V1)+ -1)*2*V+nat(V+V1)*6*V+nat(-V+V1)+nat(V+V1+1)])+1
Asymptotic class: n^2
* Total analysis performed in 397 ms.